$\forall$${\it es}$:ES.
\\[0ex]es{-}Trans(${\it es}$)
\\[0ex]$\in$ $i$:Id$\rightarrow$$k$:Knd$\rightarrow$kindcase($k$; $a$.es{-}V(${\it es}$)($i$,$a$); $l$,$t$.es{-}M(${\it es}$)($l$,$t$) )$\rightarrow$state@$i$$\rightarrow$state@$i$